Section: New Results

Model Quality

Our work on model quality defends the idea that there is not a silver bullet technique to verify the quality of models and that a combined approach offers the best trade-off. Lightweight techniques can provide a quick feedback even if it is partial and, when necessary, more complete ones can be utilized to complement the results. In this sense, this year we have developed:

• Lightweight techniques for the verification of ATL transformations [27] and UML Executable models [26]

• Proposed a method for the automatic generation of correct dynamic models for a given domain [11] . Basic operations to modify the information the software needs to store and manipulate about the domain are generated. The generation process ensures that all generated operations are strongly executable.

• Created a brand new Eclipse Lab project aimed at facilitating the verification of any kind of (EMF-based) model with the EMFtoCSP tool (see the tool description in the tools section of this report)

• And applied some of these ideas to the verification and testing of web applications [15]